T:Type, as:T List, f, g:(T).
priority-select(f;g;as) = inr()  +Unit  (aas. f(a) & g(a)) 

latex

Definitions	t  T, x:A. B(x), b, A, P & Q, Prop, x. t(x), xL. P(x), P  Q, P  Q, P  Q, ||as||, i  j < k, False, AB, {i..j}, l[i], , , priority-select(f;g;as), Unit, , A & B, x:A. B(x), (x  l)
Lemmas	l member wf, select member, le wf, priority-select-property, iff functionality wrt iff, unit wf, priority-select wf, it wf, bool wf, int seg wf, select wf, length wf1, l all wf, not wf, assert wf